﻿module Lambda

let inline private (=&=) a b = System.Object.ReferenceEquals(a, b)

open Microsoft.FSharp.Quotations
open Microsoft.FSharp.Quotations.Patterns

open Combinators

type Expr with
    member this.OccursFree x =
        Seq.exists ((=) x) (this.GetFreeVars())

    member this.AsCombinator =
        let rec asCombinator (expr: Expr): Expr =
            match expr with
            | x when x =&= S || x =&= I || x =&= K -> x
            | Var(x) -> expr
            | Lambda(x, Application(e, Var(var1))) when x = var1 && not(e.OccursFree x) ->
                asCombinator e
            | Lambda(x, e) when not(e.OccursFree x) ->
                Expr.Application(K, asCombinator e)
            | Lambda(v1, Var(v2)) when v1 = v2 -> upcast I
            | Lambda(x, Lambda(y, e)) when e.OccursFree x ->
                asCombinator <| Expr.Lambda(x, asCombinator <| Expr.Lambda(y, e))
            | Lambda(x, Application(e1, e2)) ->
                Expr.Application(
                    Expr.Application(S, asCombinator <| Expr.Lambda(x, e1)),
                    asCombinator <| Expr.Lambda(x, e2))
            | _ -> failwith "not enough rules!"
        asCombinator this

type Term<'a when 'a: equality> =
    | Variable of 'a
    | Tlambda of 'a * Term<'a>
    | Lapp of Term<'a> * Term<'a>

    member this.Var =
        match this with
        | Variable(var) -> var
        | _ -> invalidOp "this is not a variable"
    
    member this.OccursFree variable =
        match this with
        | Variable(var) -> var = variable
        | Tlambda(var, e) ->
            if var = variable then false
            else e.OccursFree variable
        | Lapp(t1, t2) -> t1.OccursFree variable || t2.OccursFree variable

    member this.Remap mapper =
        match this with
        | Variable(a) -> Variable(mapper a)
        | Tlambda(a, e) -> Tlambda(mapper a, e.Remap mapper)
        | Lapp(t1, t2) -> Lapp(t1.Remap mapper, t2.Remap mapper)

    member this.AsCombinator =
        let this = this.Remap CEvar
        let S, K, I = Variable SEcomb, Variable KEcomb, Variable IEcomb
        let rec asCombinator term =
            match term with
            | Variable(x) -> Variable(x)
            // I
            | Tlambda(x, Variable y) when x = y -> I
            // S
            | Tlambda(f, Tlambda(g, Tlambda(x,
                    Lapp(Lapp(Variable f', Variable x'),
                         Lapp(Variable g', Variable x''))))) when
                f = f' && g = g' && x = x' && x = x'' -> S
            // K
            | Tlambda(i, Tlambda(j, Variable i')) when i = i' -> K
            | Lapp(e1, e2) ->
                let c1 = asCombinator e1
                let c2 = asCombinator e2
                Lapp(c1, c2)
            | Tlambda(x, Tlambda(y, e)) when e.OccursFree x ->
                asCombinator <| Tlambda(x, asCombinator <| Tlambda(y, e))
            | Tlambda(x, Lapp(e, Variable(var1))) when x = var1 && not(e.OccursFree x) ->
                asCombinator e
            | Tlambda(var, e) when not(e.OccursFree var) ->
                Lapp(K, asCombinator e)
            | Tlambda(var1, Variable(var2)) when var1 = var2 -> I
            | Tlambda(x, Lapp(e1, e2)) ->
                Lapp(
                    Lapp(S, asCombinator <| Tlambda(x, e1)),
                    asCombinator <| Tlambda(x, e2))
            | _ -> failwith "not enough rules!"

        asCombinator this

    member this.ToString brac =
        match this with
        | Variable(var) -> sprintf "%O" var
        | Tlambda(var, e) -> sprintf "λ%O.%s" var (e.ToString true)
        | Lapp(e1, e2) ->
            sprintf 
                (if brac then "(%s %s)" else "%s %s") 
                (e1.ToString false)
                (e2.ToString true)

    override this.ToString() = this.ToString false

let rec asCombinator mterm =
    match mterm with
    | Variable(x) -> Variable(x)
    // I
    | Tlambda(x, Variable y) when x = y -> Variable(IEcomb)
    // S
    | Tlambda(f, Tlambda(g, Tlambda(x,
            Lapp(Lapp(Variable f', Variable x'),
                    Lapp(Variable g', Variable x''))))) when
        f = f' && g = g' && x = x' && x = x'' -> Variable(SEcomb)
    // K
    | Tlambda(i, Tlambda(j, Variable i')) when i = i' -> Variable(KEcomb)
    | Lapp(e1, e2) ->
        let c1 = asCombinator e1
        let c2 = asCombinator e2
        Lapp(c1, c2)
    | Tlambda(x, Tlambda(y, e)) when e.OccursFree x ->
        asCombinator <| Tlambda(x, asCombinator <| Tlambda(y, e))
    | Tlambda(x, Lapp(e, Variable(var1))) when x = var1 && not(e.OccursFree x) ->
        asCombinator e
    | Tlambda(var, e) when not(e.OccursFree var) ->
        Lapp(Variable(KEcomb), asCombinator e)
    | Tlambda(x, Lapp(e1, e2)) ->
        Lapp(
            Lapp(Variable(SEcomb), asCombinator <| Tlambda(x, e1)),
            asCombinator <| Tlambda(x, e2))
    | _ -> failwith "not enough rules!"

type VariableAllocator() =
    let var = ref 0
    member this.Alloc() =
        let value = !var
        incr var
        value
